Nuprl Lemma : increasing_lower_bound
11,40
postcript
pdf
k
:
,
f
:(int_seg(0;
k
)
),
x
:int_seg(0;
k
). increasing(
f
;
k
)
(((
f
(0)) +
x
)
(
f
(
x
)))
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
prop{i:l}
,
False
,
A
,
P
Q
,
lelt(
i
;
j
;
k
)
,
A
B
,
int_seg(
i
;
j
)
,
,
increasing(
f
;
k
)
Lemmas
nat
wf
,
int
seg
wf
,
increasing
wf
,
le
wf
,
int
seg
properties
origin
k:
, f:(int_seg(0; k)
), x:int_seg(0; k). increasing(f; k) 
(((f(0)) + x) 
(f(x))) k:, f:(int_seg(0; k)), x:int_seg(0; k). increasing(f; k) (((f(0)) + x) (f(x))) 
T Qx:A. B(x)
A
Q B